Nuprl Definition : ma-init
0,22
postcript
pdf
M
.init(
x
,
v
) ==
x0
!= 1of(2of(2of(
M
)))(
x
)
v
=
x0
latex
clarification:
M
.init(
x
,
v
)
== fpf-val(IdDeq; 1of(2of(2of(
M
)));
x
;
a
,
x0
.(
v
=
x0
fpf-cap(1of(
M
);IdDeq;
x
;Void)))
latex
Definitions
M
.init(
x
,
v
)
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
2of(
t
)
,
f
(
x
)?
z
,
1of(
t
)
,
IdDeq
FDL editor aliases
ma-init
origin
v = x0
fpf-cap(1of(M);IdDeq;x;Void))) v = x0
fpf-cap(1of(M);IdDeq;x;Void))) P(a;z)